Power preservation is a critical issue in energy-constrained systems. In order to preserve the power in these energy-constrained systems, power saving protocols such as Sleep Wakeup protocol may be implemented. The implementation of the Sleep Wakeup protocol may enable automatic switching of a node connected in a network between a power-saving mode and power-consumption mode depending on the requirement of power by the node in order to execute designated tasks of communication in the network. The power-saving mode and the power-consumption mode may also be referred as a Sleep mode and a Wakeup mode respectively. The Sleep Wakeup protocol may switch a standalone node which is not connected in the network or a node connected in the network into the Sleep mode when the communication is not required or no task is available for execution by the node. Similarly, the Sleep Wakeup protocol may switch the standalone/network node from the Sleep mode to the Wakeup mode as soon as the communication is required or a task is available for execution by the node. Thus, by implementing the Sleep Wakeup protocol in the standalone node or the network node, the energy consumption is minimized.
In general, the Sleep Wakeup protocol may be implemented in a microcontroller installed at each of the sensor nodes in the network. The Sleep Wakeup protocol may be coded in a programming language and further implemented in a system through an application, wherein the application may be configured to execute the Sleep Wakeup Protocol. The implementation of the Sleep Wakeup protocol may require its verification in order to check whether state transitions of the protocol are conforming to the specifications of the microcontroller. For the system implementing the Sleep Wakeup protocol, it is very difficult to verify whether the state transitions (Sleep/Wakeup) are conforming to the specifications of the microcontroller. Such verification is required in order to detect if its implementation will not lead to unexpected behavior at run-time. Few examples of the unexpected behavior may be Battery Drain, and Watch Dog timer reset etc. In the existing state of art, this verification is done manually and is generally found to be time consuming, costly and sometimes error-prone. Therefore, an automated technique for this type of verification is required in the current state of the art that can detect the defects that may occur during the transition of the microcontroller from the Low Power Consumption (Sleep) to High Power Consumption (Wakeup) modes and vice versa.